Về mặt logic, nhiều định lý có dạng một điều kiện chỉ định: Nếu A, thì B. Một định lý như vậy không khẳng định B - chỉ nói rằng B là hệ quả cần thiết của A. Trong trường hợp này, A được gọi là giả thiết của định lý ("giả thuyết" ở đây có nghĩa là một cái gì đó rất khác với một phỏng đoán), và B là kết luận của định lý. Cả hai phần này đặt cạnh nhau (không cần chứng minh) được gọi là mệnh đề hoặc phát biểu của định lý (ví dụ "Nếu A, thì B" là mệnh đề). Ngoài ra, A và B cũng có thể được gọi là tiền đề và hậu quả.[9] Định lý "Nếu n là số tự nhiên chẵn thì n/2 là số tự nhiên" là một ví dụ điển hình trong đó giả thuyết là "n là số tự nhiên chẵn", và kết luận là "n/2 cũng là số tự nhiên".

Để một định lý được chứng minh, về nguyên tắc nó phải có thể diễn đạt được như một phát biểu chính xác về mặt hình thức. Tuy nhiên, các định lý thường được diễn đạt bằng ngôn ngữ tự nhiên chứ không phải ở dạng ký hiệu hoàn toàn - với giả định rằng một tuyên bố hình thức của định lý có thể được rút ra từ một tuyên bố phi hình thức.

Trong toán học, người ta thường chọn một số giả thuyết trong một ngôn ngữ nhất định và tuyên bố rằng lý thuyết bao gồm tất cả các phát biểu có thể chứng minh được từ các giả thuyết này. Những giả thuyết này tạo thành cơ sở nền tảng của lý thuyết và được gọi là tiên đề hay định đề. Lĩnh vực toán học được gọi là lý thuyết chứng minh nghiên cứu các ngôn ngữ hình thức, tiên đề và cấu trúc của phép chứng minh.

Một bản đồ phẳng có năm màu sao cho không có hai vùng có cùng màu gặp nhau. Nó thực sự có thể được tô màu theo cách này chỉ với bốn màu. Định lý bốn màu nói rằng việc tô màu như vậy có thể sử dụng được cho bất kỳ bản đồ phẳng nào, nhưng mọi chứng minh đã biết đều liên quan đến một tìm kiếm tính toán quá lâu để có thể kiểm tra bằng tay.

Một số định lý là "tầm thường", theo nghĩa là chúng tuân theo các định nghĩa, tiên đề và các định lý khác theo những cách hiển nhiên và không chứa đựng bất kỳ hiểu biết đáng ngạc nhiên nào.[10] Mặt khác, một số định lý có thể được gọi là "sâu", bởi vì các chứng minh của chúng có thể dài và khó, liên quan đến các lĩnh vực toán học khác không liên quan với tuyên bố của chính định lý, hoặc cho thấy các mối liên hệ đáng ngạc nhiên giữa các lĩnh vực toán học khác nhau.[11] Một định lý có thể được phát biểu rất đơn giản nhưng rất sâu sắc. Một ví dụ tuyệt vời cho việc này là Định lý cuối cùng của Fermat,[12] và có nhiều ví dụ khác về các định lý đơn giản nhưng sâu sắc trong lý thuyết số và tổ hợp, và các lĩnh vực khác.

Các định lý khác có chứng minh đã biết mà không thể dễ dàng viết ra. Các ví dụ nổi bật nhất cho việc này là định lý bốn màu và giả thuyết Kepler. Cả hai định lý này chỉ được biết là đúng bằng cách rút gọn chúng thành một tìm kiếm tính toán sau đó được một chương trình máy tính xác minh. Ban đầu, nhiều nhà toán học không chấp nhận hình thức chứng minh này, nhưng bây giờ nó đã được chấp nhận rộng rãi hơn. Nhà toán học Doron Zeilberger thậm chí đã đi xa đến mức tuyên bố rằng đây có thể là những kết quả tầm thường duy nhất mà các nhà toán học đã từng chứng minh.[13] Nhiều định lý toán học có thể được rút gọn thành tính toán đơn giản hơn, bao gồm các nhận dạng đa thức, nhận dạng lượng giác [14] và các nhận dạng siêu hình học.[15]